M.rframe(A.sends tfL of k on l)
== xdom(1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M)))))))))))). 

== L=1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M)))))))))))(x)  
== Ldeq-member(KindDeq;k;L)
==  (s1, s2:A.state, v:A.da(k).
==  ((s1  s2 mod x)  (i:||tfL||. 2of(tfL[i])(s1,v) = 2of(tfL[i])(s2,v))) 

latex

---

clarification:

M.rframe(A.sends tfL of k on l)
== fpf-all(Id;
== fpf-all(IdDeq;
== fpf-all(1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M)))))))))));
== fpf-all(x,L.(deq-member(KindDeq;k;L)
== fpf-all( (s1:A.state, s2:A.state, v:A.da(k).
== fpf-all( (ma-x-equiv(A;x;s1;s2)
== fpf-all( ( (i:{0..||tfL||}.
== fpf-all( ( (2of(tfL[i])(s1,v) = 2of(tfL[i])(s2,v)  A.dout(l,1of(tfL[i])) List)))) 

latex

Definitions	xdom(f). v=f(x)   P(x;v), Id, IdDeq, P  Q, b, deq-member(eq;x;L), KindDeq, M.state, M.da(a), P  Q, (s1  s2 mod x), x:A. B(x), {i..j}, #$n, ||as||, s = t, type List, M.dout(l,tg), 1of(t), f(a), 2of(t), l[i]
FDL editor aliases	ma-rframe-send